$\forall$$A$:Realizer, $x$:Knd.
\\[0ex]($\neg$($\uparrow$Rplus?($A$)))
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$Rnone?($A$)))
\\[0ex]$\Rightarrow$ ($\uparrow$$x$ $\in$ dom(Rda($A$)))
\\[0ex]$\Rightarrow$ (inl locknd(R{-}loc($A$);$x$)  $\in$ R{-}names($A$))